Nuprl Lemma : for_hdtl_wf
2,24
postcript
pdf
A
,
B
,
C
:Type,
f
:(
B
C
C
),
k
:
C
,
as
:
A
List,
g
:(
A
(
A
List)
B
).
(ForHdTl{
A
,
f
,
k
}
h
::
t
as
.
g
(
h
,
t
))
C
latex
Definitions
t
T
,
x
(
s1
,
s2
)
,
x
:
A
.
B
(
x
)
,
mapcons(
f
;
as
)
,
reduce(
f
;
k
;
as
)
,
ForHdTl{
A
,
f
,
k
}
h
::
t
as
.
g
(
h
;
t
)
Lemmas
reduce
wf
,
mapcons
wf
origin
A, B, C:Type, f:(B
CC), k:C, as:A List, g:(A(A List)B).
as. g(h,t)) C A, B, C:Type, f:(BCC), k:C, as:A List, g:(A(A List)B).
as. g(h,t)) C Tx:A. B(x) as. g(h;t)